\begin{tabbing}
ecl{-}halt(${\it ds}$;${\it da}$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl\_ind($x$;$k$,${\it test}$.$\lambda$$n$,$L$. $n$ $=$ 0 $\in$ $\mathbb{Z}$\+
\\[0ex]\& (\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, $s$:State(${\it ds}$), $v$:Valtype(${\it da}$;$k$).\+
\\[0ex]$L$ $=$ (${\it L'}$ @ ($\langle$$k$$,\,$$s$$,\,$$v$$\rangle$.nil)) $\in$ event{-}info(${\it ds}$;${\it da}$) List \& ${\it test}$($s$,$v$)
\\[0ex]\& l\_all(${\it L'}$;event{-}info(${\it ds}$;${\it da}$);$t$.$\neg$\=let ${\it k'}$,$s$,$v$ = $t$ in \+
\\[0ex]$k$ $=$ ${\it k'}$ $\in$ Knd \& ${\it test}$($s$,$v$)));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$. 0$<$$n$
\-\-\\[0ex]\& ${\it ha}$($n$,$L$)
\\[0ex]$\vee$ (\=$\exists$$L_{1}$:event{-}info(${\it ds}$;${\it da}$) List, $L_{2}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]$L$ $=$ ($L_{1}$ @ $L_{2}$) $\in$ event{-}info(${\it ds}$;${\it da}$) List \& ${\it ha}$(0,$L_{1}$) \& ${\it hb}$($n$,$L_{2}$));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$.
\-\\[0ex](\=$n$ $=$ 0 $\in$ $\mathbb{Z}$\+
\\[0ex]$\Rightarrow$ \=${\it ha}$(0,$L$)\+
\\[0ex]\& ($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& ${\it hb}$(0,${\it L'}$))
\\[0ex]$\vee$ \=${\it hb}$(0,$L$)\+
\\[0ex]\& ($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& ${\it ha}$(0,${\it L'}$)))
\-\-\-\\[0ex]\& (\=0$<$$n$\+
\\[0ex]$\Rightarrow$ \=${\it ha}$($n$,$L$)\+
\\[0ex]\& (\=$\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ ${\it hb}$($m$,${\it L'}$)
\\[0ex]$\Rightarrow$ ${\it L'}$ $=$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& $n$$\leq$$m$)
\-\\[0ex]$\vee$ \=${\it hb}$($n$,$L$)\+
\\[0ex]\& (\=$\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ ${\it ha}$($m$,${\it L'}$)
\\[0ex]$\Rightarrow$ ${\it L'}$ $=$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& $n$$\leq$$m$));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$. ${\it ha}$($n$,$L$)
\-\-\-\-\\[0ex]\& (\=$\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ ${\it hb}$($m$,${\it L'}$)
\\[0ex]$\Rightarrow$ ${\it L'}$ $=$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& $n$$\leq$$m$)
\-\\[0ex]$\vee$ \=${\it hb}$($n$,$L$)\+
\\[0ex]\& (\=$\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ ${\it ha}$($m$,${\it L'}$)
\\[0ex]$\Rightarrow$ ${\it L'}$ $=$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List \& $n$$\leq$$m$);$a$,${\it ha}$.$\lambda$$n$,$L$. 0$<$$n$
\-\-\\[0ex]\& star{-}append(event{-}info(${\it ds}$;${\it da}$);${\it ha}$(0);${\it ha}$($n$))($L$);$a$,$m$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.$\lambda$$n$,$L$. 0$<$$n$ \& ${\it ha}$($n$,$L$)
\\[0ex]$\vee$ $n$ $=$ $m$ $\in$ $\mathbb{Z}$ \& ${\it ha}$(0,$L$);$a$,$l$,${\it ha}$.$\lambda$$n$,$L$. ${\it ha}$($n$,$L$) \& $\neg$($n$ $\in$ $l$ $\in$ $\mathbb{N}$)
\\[0ex]$\vee$ $n$ $=$ 0 $\in$ $\mathbb{Z}$ \& l\_exists($l$;$\mathbb{N}$;$m$.${\it ha}$($m$,$L$)))
\-
\end{tabbing}